Nuprl Lemma : fpf-sub-join-left2 11,40
A:Type, B:(AType), eq:EqDecider(A), f,h,g:fpf(A; a.B(a)).
fpf-sub(A; a.B(a); eq; h; f)  fpf-sub(A; a.B(a); eq; h; fpf-join(eq; f; g)) 
latex

Definitionst  T, x(s), x:A. B(x), x. t(x), fpf-sub(A; a.B(a); eq; f; g), P  Q, EqDecider(T), fpf(A; a.B(a)), fpf-join(eq; f; g)
Lemmasfpf-sub wf, fpf wf, deq wf, fpf-sub transitivity, fpf-join wf, fpf-sub-join-left

origin